$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $P$:($A$$\rightarrow$Type$\rightarrow\mathbb{P}$), $f$, $g$:$x$:$A$ fp$\rightarrow$ Type.
\\[0ex]$\forall$$y$$\in$dom($f$). $w$=$f$($y$) $\Rightarrow$  $P$($y$,$w$)
\\[0ex]$\Rightarrow$ $\forall$$y$$\in$dom($g$). $w$=$g$($y$) $\Rightarrow$  $P$($y$,$w$)
\\[0ex]$\Rightarrow$ $\forall$$y$$\in$dom($f$ $\oplus$ $g$). $w$=$f$ $\oplus$ $g$($y$) $\Rightarrow$  $P$($y$,$w$)